Termination of the following Term Rewriting System could be proven:
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(X, g(X), Y) → f(Y, Y, Y)
g(b) → c
b → c
The replacement map contains the following entries:f: empty set
g: {1}
b: empty set
c: empty set
↳ CSR
↳ CSDependencyPairsProof
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(X, g(X), Y) → f(Y, Y, Y)
g(b) → c
b → c
The replacement map contains the following entries:f: empty set
g: {1}
b: empty set
c: empty set
Using Improved CS-DPs we result in the following initial Q-CSDP problem.
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
Q-restricted context-sensitive dependency pair problem:
The symbols in {g} are replacing on all positions.
The symbols in {f, F} are not replacing on any position.
The ordinary context-sensitive dependency pairs DPo are:
F(X, g(X), Y) → F(Y, Y, Y)
The TRS R consists of the following rules:
f(X, g(X), Y) → f(Y, Y, Y)
g(b) → c
b → c
Q is empty.
The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.
The rules F(z0, g(z0), z1) → F(z1, z1, z1) and F(x0, g(x0), x1) → F(x1, x1, x1) form no chain, because ECapµ(F(z1, z1, z1)) = F(z1, z1, z1) does not unify with F(x0, g(x0), x1).